ds:fpf(Id; x.Type), da:fpf(Knd; k.Type). msg-spec(ds; da)  Type 

latex

Definitions	Id, t  T, Type, x. t(x), x:A. B(x), fpf(A; a.B(a)), Knd, IdLnk, x:A  B(x), x.A(x), t.2, t.1, msg-item(ds; da; k; l), type List, msg-spec(ds; da)
Lemmas	msg-item wf, pi1 wf, pi2 wf, IdLnk wf, Knd wf, fpf wf, Id wf